A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a).
(x:A. x  dom(f) & x  dom(g)  B(x)  C(x) & f(x) = g(x)  C(x))  g  f  g 

latex

Definitions	2of(t), f  g, f(x)?z, Unit, , b, A, P  Q, P  Q, P  Q, {T}, EqDecider(T), Prop, f(x), P & Q, f  g, P  Q, x  dom(f), a:A fp B(a), Top, x. t(x), x:A. B(x), x(s), t  T, A & B, b
Lemmas	fpf-trivial-subtype-top, fpf-dom wf, assert wf, fpf-ap wf, fpf wf, deq wf, fpf-join-dom2, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert